basic
\\[0ex]Irrefl($T$;$x$,$y$.$E$($x$;$y$)) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$a$:$T$. $\neg$$E$($a$;$a$)